empty(nil) → true
empty(cons(x, y)) → false
tail(nil) → nil
tail(cons(x, y)) → y
head(cons(x, y)) → x
zero(0) → true
zero(s(x)) → false
p(0) → 0
p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))
intlist(x) → if_intlist(empty(x), x)
if_intlist(true, x) → nil
if_intlist(false, x) → cons(s(head(x)), intlist(tail(x)))
int(x, y) → if_int(zero(x), zero(y), x, y)
if_int(true, b, x, y) → if1(b, x, y)
if_int(false, b, x, y) → if2(b, x, y)
if1(true, x, y) → cons(0, nil)
if1(false, x, y) → cons(0, int(s(0), y))
if2(true, x, y) → nil
if2(false, x, y) → intlist(int(p(x), p(y)))
↳ QTRS
↳ DependencyPairsProof
empty(nil) → true
empty(cons(x, y)) → false
tail(nil) → nil
tail(cons(x, y)) → y
head(cons(x, y)) → x
zero(0) → true
zero(s(x)) → false
p(0) → 0
p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))
intlist(x) → if_intlist(empty(x), x)
if_intlist(true, x) → nil
if_intlist(false, x) → cons(s(head(x)), intlist(tail(x)))
int(x, y) → if_int(zero(x), zero(y), x, y)
if_int(true, b, x, y) → if1(b, x, y)
if_int(false, b, x, y) → if2(b, x, y)
if1(true, x, y) → cons(0, nil)
if1(false, x, y) → cons(0, int(s(0), y))
if2(true, x, y) → nil
if2(false, x, y) → intlist(int(p(x), p(y)))
IF_INT(false, b, x, y) → IF2(b, x, y)
IF1(false, x, y) → INT(s(0), y)
INTLIST(x) → IF_INTLIST(empty(x), x)
INT(x, y) → IF_INT(zero(x), zero(y), x, y)
IF_INTLIST(false, x) → TAIL(x)
IF_INTLIST(false, x) → INTLIST(tail(x))
IF2(false, x, y) → P(x)
IF_INT(true, b, x, y) → IF1(b, x, y)
IF_INTLIST(false, x) → HEAD(x)
IF2(false, x, y) → INTLIST(int(p(x), p(y)))
P(s(s(x))) → P(s(x))
INT(x, y) → ZERO(y)
INT(x, y) → ZERO(x)
IF2(false, x, y) → P(y)
IF2(false, x, y) → INT(p(x), p(y))
INTLIST(x) → EMPTY(x)
empty(nil) → true
empty(cons(x, y)) → false
tail(nil) → nil
tail(cons(x, y)) → y
head(cons(x, y)) → x
zero(0) → true
zero(s(x)) → false
p(0) → 0
p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))
intlist(x) → if_intlist(empty(x), x)
if_intlist(true, x) → nil
if_intlist(false, x) → cons(s(head(x)), intlist(tail(x)))
int(x, y) → if_int(zero(x), zero(y), x, y)
if_int(true, b, x, y) → if1(b, x, y)
if_int(false, b, x, y) → if2(b, x, y)
if1(true, x, y) → cons(0, nil)
if1(false, x, y) → cons(0, int(s(0), y))
if2(true, x, y) → nil
if2(false, x, y) → intlist(int(p(x), p(y)))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
IF_INT(false, b, x, y) → IF2(b, x, y)
IF1(false, x, y) → INT(s(0), y)
INTLIST(x) → IF_INTLIST(empty(x), x)
INT(x, y) → IF_INT(zero(x), zero(y), x, y)
IF_INTLIST(false, x) → TAIL(x)
IF_INTLIST(false, x) → INTLIST(tail(x))
IF2(false, x, y) → P(x)
IF_INT(true, b, x, y) → IF1(b, x, y)
IF_INTLIST(false, x) → HEAD(x)
IF2(false, x, y) → INTLIST(int(p(x), p(y)))
P(s(s(x))) → P(s(x))
INT(x, y) → ZERO(y)
INT(x, y) → ZERO(x)
IF2(false, x, y) → P(y)
IF2(false, x, y) → INT(p(x), p(y))
INTLIST(x) → EMPTY(x)
empty(nil) → true
empty(cons(x, y)) → false
tail(nil) → nil
tail(cons(x, y)) → y
head(cons(x, y)) → x
zero(0) → true
zero(s(x)) → false
p(0) → 0
p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))
intlist(x) → if_intlist(empty(x), x)
if_intlist(true, x) → nil
if_intlist(false, x) → cons(s(head(x)), intlist(tail(x)))
int(x, y) → if_int(zero(x), zero(y), x, y)
if_int(true, b, x, y) → if1(b, x, y)
if_int(false, b, x, y) → if2(b, x, y)
if1(true, x, y) → cons(0, nil)
if1(false, x, y) → cons(0, int(s(0), y))
if2(true, x, y) → nil
if2(false, x, y) → intlist(int(p(x), p(y)))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDP
INTLIST(x) → IF_INTLIST(empty(x), x)
IF_INTLIST(false, x) → INTLIST(tail(x))
empty(nil) → true
empty(cons(x, y)) → false
tail(nil) → nil
tail(cons(x, y)) → y
head(cons(x, y)) → x
zero(0) → true
zero(s(x)) → false
p(0) → 0
p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))
intlist(x) → if_intlist(empty(x), x)
if_intlist(true, x) → nil
if_intlist(false, x) → cons(s(head(x)), intlist(tail(x)))
int(x, y) → if_int(zero(x), zero(y), x, y)
if_int(true, b, x, y) → if1(b, x, y)
if_int(false, b, x, y) → if2(b, x, y)
if1(true, x, y) → cons(0, nil)
if1(false, x, y) → cons(0, int(s(0), y))
if2(true, x, y) → nil
if2(false, x, y) → intlist(int(p(x), p(y)))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
INTLIST(x) → IF_INTLIST(empty(x), x)
Used ordering: Polynomial interpretation [25,35]:
IF_INTLIST(false, x) → INTLIST(tail(x))
The value of delta used in the strict ordering is 1/16.
POL(IF_INTLIST(x1, x2)) = (1/4)x_1 + (3/4)x_2
POL(empty(x1)) = 3/4 + (4)x_1
POL(cons(x1, x2)) = 1/2 + (4)x_2
POL(tail(x1)) = (1/4)x_1
POL(true) = 3/4
POL(false) = 1
POL(INTLIST(x1)) = 1/4 + (2)x_1
POL(nil) = 0
empty(nil) → true
tail(nil) → nil
empty(cons(x, y)) → false
tail(cons(x, y)) → y
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDP
IF_INTLIST(false, x) → INTLIST(tail(x))
empty(nil) → true
empty(cons(x, y)) → false
tail(nil) → nil
tail(cons(x, y)) → y
head(cons(x, y)) → x
zero(0) → true
zero(s(x)) → false
p(0) → 0
p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))
intlist(x) → if_intlist(empty(x), x)
if_intlist(true, x) → nil
if_intlist(false, x) → cons(s(head(x)), intlist(tail(x)))
int(x, y) → if_int(zero(x), zero(y), x, y)
if_int(true, b, x, y) → if1(b, x, y)
if_int(false, b, x, y) → if2(b, x, y)
if1(true, x, y) → cons(0, nil)
if1(false, x, y) → cons(0, int(s(0), y))
if2(true, x, y) → nil
if2(false, x, y) → intlist(int(p(x), p(y)))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
P(s(s(x))) → P(s(x))
empty(nil) → true
empty(cons(x, y)) → false
tail(nil) → nil
tail(cons(x, y)) → y
head(cons(x, y)) → x
zero(0) → true
zero(s(x)) → false
p(0) → 0
p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))
intlist(x) → if_intlist(empty(x), x)
if_intlist(true, x) → nil
if_intlist(false, x) → cons(s(head(x)), intlist(tail(x)))
int(x, y) → if_int(zero(x), zero(y), x, y)
if_int(true, b, x, y) → if1(b, x, y)
if_int(false, b, x, y) → if2(b, x, y)
if1(true, x, y) → cons(0, nil)
if1(false, x, y) → cons(0, int(s(0), y))
if2(true, x, y) → nil
if2(false, x, y) → intlist(int(p(x), p(y)))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
P(s(s(x))) → P(s(x))
The value of delta used in the strict ordering is 16.
POL(P(x1)) = (4)x_1
POL(s(x1)) = 1 + (4)x_1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
empty(nil) → true
empty(cons(x, y)) → false
tail(nil) → nil
tail(cons(x, y)) → y
head(cons(x, y)) → x
zero(0) → true
zero(s(x)) → false
p(0) → 0
p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))
intlist(x) → if_intlist(empty(x), x)
if_intlist(true, x) → nil
if_intlist(false, x) → cons(s(head(x)), intlist(tail(x)))
int(x, y) → if_int(zero(x), zero(y), x, y)
if_int(true, b, x, y) → if1(b, x, y)
if_int(false, b, x, y) → if2(b, x, y)
if1(true, x, y) → cons(0, nil)
if1(false, x, y) → cons(0, int(s(0), y))
if2(true, x, y) → nil
if2(false, x, y) → intlist(int(p(x), p(y)))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
IF_INT(false, b, x, y) → IF2(b, x, y)
IF1(false, x, y) → INT(s(0), y)
INT(x, y) → IF_INT(zero(x), zero(y), x, y)
IF_INT(true, b, x, y) → IF1(b, x, y)
IF2(false, x, y) → INT(p(x), p(y))
empty(nil) → true
empty(cons(x, y)) → false
tail(nil) → nil
tail(cons(x, y)) → y
head(cons(x, y)) → x
zero(0) → true
zero(s(x)) → false
p(0) → 0
p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))
intlist(x) → if_intlist(empty(x), x)
if_intlist(true, x) → nil
if_intlist(false, x) → cons(s(head(x)), intlist(tail(x)))
int(x, y) → if_int(zero(x), zero(y), x, y)
if_int(true, b, x, y) → if1(b, x, y)
if_int(false, b, x, y) → if2(b, x, y)
if1(true, x, y) → cons(0, nil)
if1(false, x, y) → cons(0, int(s(0), y))
if2(true, x, y) → nil
if2(false, x, y) → intlist(int(p(x), p(y)))